(declare-fun a () Real)
(declare-fun d () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun o () Real)
(declare-fun g () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun m () Real)
(assert (or (not (exists ((h Real)) (=> (and (= (<= h (/ d k)) (>= (+ (* c h) (/ b m)) 0)) (>= o 0)) (<= g (* (/ 1 2) (+ (* c (/ d k) (/ d k)) (* (* 2 (/ d k)) o) (* 2 g))))))) (not (exists ((i Real)) (=> (> l 0) (= (>= e 0) (= (= (<= i e) (<= 0 f)) (= m 2))))))))
(assert (= a (/ a c)))
(assert (= o m (/ b o)))
(check-sat)
